a, b:. ((a * b) < 0)  (((a < 0) & (b > 0))  ((a > 0) & (b < 0))) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), P  Q, T, P  Q, P  Q, , True, P & Q, P  Q, i > j
Lemmas	pos mul arg bounds, true wf, squash wf, iff wf, gt wf, and functionality wrt iff, or functionality wrt iff, minus mono wrt lt, iff functionality wrt iff